\documentclass[dvipsnames]{report}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage[top=2cm, bottom=2cm, left=2cm, right=2cm]{geometry}
\usepackage{array}
\usepackage{amsmath}
\usepackage{pgfplots}
\usepackage{tikz}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{listings}
\usepackage{color}
\usepackage{float}
\usepackage{tabularx}
\usetikzlibrary{arrows,positioning,automata,shadows,fit,shapes}

\newcommand{\figscale}[1]{\scalebox{0.9}{#1}}
\renewcommand{\thesection}{\arabic{section}}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}

\lstset{% This applies to ALL lstlisting
    backgroundcolor=\color{white!10},%
  language=Java,                % the language of the code
  basicstyle=\footnotesize,           % the size of the fonts that are used for the code
  showspaces=false,               % show spaces adding particular underscores
  showstringspaces=false,         % underline spaces within strings
  showtabs=false,                 % show tabs within strings adding particular underscores
  frame=single,                   % adds a frame around the code
  rulecolor=\color{black},        % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
  tabsize=2,                      % sets default tabsize to 2 spaces
  keywordstyle=\color{blue},          % keyword style
  commentstyle=\color{gray},
  captionpos=b,
  literate={á}{{\'a}}1 {ã}{{\~a}}1 {é}{{\'e}}1 {è}{{\`e}}1 {à}{{\`a}}1,
    }%

\protected\def\psverb#1{\def\innerpsverb##1#1{\texttt{##1}}\innerpsverb}

\def\fixcheck{%
    \def\tikzifinpicture##1##2{##2}%
}%

% type user-defined commands here

\begin{document}

\title{Modélisation et vérification}   % type title between braces
\author{Hamza Benkabbou, Kevin Bourgeois, Jérémy Morosi,\\Jean-Baptiste Perrin, Zo Rabarijaona}         % type author(s) between braces
\date{\today}    % type date between braces
\maketitle

\tableofcontents

\newpage

\section{Organisation du code}

\subsection{principal}

Ce package contient la classe \texttt{Main} du programme. Elle implémente l'interface \texttt{ICallback} (listing \ref{lst:ICallback}) qui définie toutes les fonctions demandées dans le sujet. L'intérêt de cette interface est de pouvoir passer le \texttt{Main} en paramètre du parseur \texttt{CommandLineParser}. Il a été créé avec ANTLR dans le but de pouvoir analyser simplement les commandes saisies par l'utilisateur et de pouvoir appeler les méthodes correspondantes dans le \texttt{Main} au travers de l'interface.

\subsection{CTL}

C'est le package qui contient la classe \texttt{CTL}. Outre les méthodes pour calculer la valeur d'une formule, on y trouve la méthode \texttt{valeur} qui retourne la liste des états validant une formule et la méthode \texttt{justifie} qui retourne la preuve.

\subsection{rdp}

C'est le package qui contient la classe \texttt{RdP}.

\subsection{systeme}

C'est le package qui contient les classes \texttt{AlgoGrapheRdP} et \texttt{GrapheRdP}. La classe \texttt{GrapheRdP} contient les méthodes \texttt{ctlToDot} pour afficher les états validant une formule au format \texttt{.dot} et \texttt{justifieToDot} pour la justification d'un état.

\subsection{preuve}

Ce package contient toutes les classes liées aux preuves. On y trouve les interfaces \texttt{IPreuve} (listing \ref{lst:IPreuve}) et \texttt{IChemin} (listing \ref{lst:IChemin}) qui définissent ce qu'est une preuve. On y trouve aussi une implémentation pour chaque type de preuve et les deux classes \texttt{Coloration} (listing \ref{lst:Coloration}) et \texttt{Couleur} qui gèrent la coloration. La classe \texttt{Preuve} contient, entre autres, la méthode \texttt{neg} qui retourne la négation d'une formule.

\section{Validation}

Cette partie décrit comment la formule est analysée et validée.

\subsection{Analyse}

L'analyse de la formule saisie par l'utilisateur dans le terminal se fait à l'aide d'un parseur généré par ANTLR. Grâce à ce parseur, toute formule est mise sous la forme d'un arbre (classe \texttt{Tree}) où chaque branche est un morceau de la formule originale et les feuilles sont les formules atomiques qui la composent. Pour $EX(\$A~\|~\$B)$ par exemple, on obtiendrait le résultat de la figure \ref{fig:ValidationAnalyse}. Il est ainsi plus facile d'utiliser la formule par la suite puisqu'il suffira de faire un \texttt{switch} sur le type d'un noeud et d'accéder à ses enfants en conséquence.

\input{"Rapport/validation_analyse.tex"}

\subsection{\'{E}tats valides}

La validation a lieue dans la méthode \texttt{justifie} de la classe \texttt{CTL}. Comme dit précédemment, pour parcourir la formule on utilise un \texttt{switch} et on compare le type du noeud avec les constantes identifiants les tokens dans le parseur. Pour calculer la liste des états valides, il suffit donc de partir de la racine de l'arbre, atteindre les feuilles de manière récursive, récupérer les états valides pour les formules atomiques et appliquer chaque partie de la formule petit à petit en retournant vers la racine. \`{A} la fin on dispose de la liste de tous les états validant la formule.


\section{Justification}

Cette partie décrit la manière dont le programme calcule et mémorise la justification d'une formule CTL pour ensuite en donner une représentation visuelle.

\subsection{Preuve}

L'interface \texttt{IPreuve} (listing \ref{lst:IPreuve}) définie les méthodes nécessaires pour prouver qu'une formule CTL est vraie. 

La structure d'une preuve est très simple, puisqu'elle consiste en la formule qui lui est associée (\texttt{getFormule}), en la liste des états qui sont vrais (\texttt{getMarquage}, \texttt{setMarquage}) et en la liste des sous-preuves pour chaque morceau de la formule (\texttt{getPreuves}).

Une preuve dispose aussi de plusieurs méthodes pour la visualiser. On peut récupérer la formule qui lui est associée au format textuel grâce à la méthode \texttt{formuleToString}. On peut obtenir un affichage sous forme d'arbre de la preuve et de ses sous-preuves grâce à la méthode \texttt{toTree}. On peut récupérer la formule sous la forme d'un label coloré pour l'exportation au format \texttt{.dot} grâce à la méthode \texttt{toDotLabel}. Et finalement, on peut exporter la preuve au format \texttt{.dot} grâce aux méthodes \texttt{toDotRacine} et \texttt{toDot}.

Lors du calcul de la preuve, les méthodes \texttt{couperRacine} et \texttt{couper} permettent de supprimer les états qui sont inutiles car ils n'ont pas de prédécesseurs dans la preuve parent.

\subsubsection{Création}

La création d'une preuve se fait en même temps que la validation de la formule CTL associée. Si la formule est un ensemble de sous-formules, on commence d'abord par les justifier. Ensuite, on peut créer une preuve du même type que la formule, en lui donnant le marquage la validant et la liste des sous-preuves. Au passage, on génère la couleur et le label (au format \texttt{.dot}) de la formule. Le label est l'ensemble des labels des sous-formules auxquels on ajoute le nom de la formule avec la couleur correspondante. Par exemple, pour $E(\$A \cup \$B)$, on obtient le label \texttt{<FONT COLOR="...">E(... U ...)</FONT>}.

\subsubsection{Coupage}

Une fois qu'on a construit la preuve complète, on appelle la méthode \texttt{couperRacine} en donnant en paramètre le numéro de l'état pour lequel on doit justifier la formule CTL. Cet appel a pour conséquence de mettre tous les états validant la preuve à $false$, sauf celui donné. La preuve appelle ensuite la méthode \texttt{couper} des sous-preuves en donnant son marquage en paramètre. Les sous-preuves vont alors remettre à $false$ tous les états valident qui n'ont pas de prédécesseurs dans le marquage donné, puis, elles vont à leur tour appeler la méthode pour leurs sous-preuves en donnant leur propre marquage. Ainsi, à la fin, il ne restera dans les preuves que les états qui sont réellement nécessaires à la justification.

\subsubsection{Affichage au format textuel}

L'affichage de la preuve au format textuel est assez simple. Une fois que tous les états non nécessaires ont été retirés par le coupage, on peut afficher la formule associée à la preuve, suivie de la liste des états la validant. Les sous-preuves sont affichées récursivement en appelant leur méthode \texttt{toTree} avec le niveau d'indentation désiré. On obtient alors un arbre dont la racine est la preuve complète et les dont les branches sont les formules atomiques (figure \ref{fig:PreuveAffichageTextuel}).

\input{"Rapport/preuve_affichage_textuel.tex"}

Certaines preuves plus complexes, comme les chemins, affichent les preuves pour tous les états du chemin avec le même niveau d'indentation et les entourent par des accolades (figure \ref{fig:PreuveAffichageTextuelChemin}).

\input{"Rapport/preuve_affichage_textuel_chemin.tex"}

\subsubsection{Affichage au format .dot}

L'exportation de la preuve au format \texttt{.dot} commence dans la méthode \texttt{justifieToDot} de la classe \texttt{GrapheRdP}. On appelle la méthode \texttt{toDotRacine} de la preuve complète en lui donnant en paramètres une variable de type \texttt{Map<Integer, {Set<Integer>}>} et une variable de type \texttt{Set<String>}. La première, dont les clefs sont les états du réseau de pétri et les valeurs sont les listes des états auxquels ils sont reliés, permettra à toutes les sous-preuves d'indiquer quels états sont reliés par une justification. La seconde devra contenir l'ensemble des flèches du graphe (au format \texttt{.dot}) qui font parties de la justification.

La méthode \texttt{toDotRacine} sert uniquement à appeler la méthode \texttt{toDot} pour toutes les sous-preuves sans qu'une flèche ne soit ajoutée pour l'état de départ. La méthode \texttt{toDot} permet à une preuve d'ajouter toutes les flèches nécessaires au graphe puis de s'appeler pour toutes les sous-preuves. Une flèche doit partir d'un état parent, aller vers un état validant la sous-preuve et elle doit avoir le label de la formule associée à la sous-preuve à côté.

Une fois que toutes les flèches ont été ajoutées, on commence par exporter la liste des états avec leur marquage et avec le label de la formule complète pour l'état pour lequel on doit justifier la formule (figure \ref{fig:PreuveAffichageDot1}). On exporte ensuite l'ensemble des flèches qui se trouvent dans la variable précédente (figure \ref{fig:PreuveAffichageDot2}). Puis on complète le graphe avec les flèches manquantes (celles qui ne font pas parties de la justification) (figure \ref{fig:PreuveAffichageDot3}).

\input{"Rapport/preuve_affichage_dot.tex"}

Pour l'ajout des flèches manquantes, on utilise la liste des états reliés pour savoir si elle existe déjà. La liste des flèches nous permet de nous assurer qu'une même preuve ne soit affichée qu'une fois (figure \ref{fig:PreuveAffichageDot4}).

\input{"Rapport/preuve_affichage_dot2.tex"}

\subsubsection{Coloration}

La coloration des preuves est gérée par la classe \texttt{Coloration} (listing \ref{lst:Coloration}). Son but est d'associer une couleur unique (si possible) et un label coloré (pour l'exportation au format \texttt{.dot}) à une formule. Lors de l'exportation, les accesseurs \texttt{getCouleur} et \texttt{getLabel} permettront alors de récupérer les informations liées à la formule donnée.

Les couleurs sont générées par la méthode \texttt{genererCouleur}. Dans l'idéal, toutes les couleurs utilisées doivent être uniques et ne doivent pas trop se ressembler pour que la preuve soit suffisamment claire. Ici, on génère juste des couleurs au format HSV avec $s=1$, $v=0.75$ et en incrémentant le $h$ d'une certaine valeur à chaque appel de la méthode.

La couleur d'une formule est utilisée pour colorer une flèche partant d'un état validant la formule et allant vers un état validant une sous-formule alors que le label de la sous-formule est affiché sur la flèche (figure \ref{fig:Coloration}).

\input{"Rapport/preuve_coloration.tex"}

\subsection{Preuves atomiques}

Les preuves atomiques sont les preuves associées aux formules atomiques $p$, $true$, $false$, $dead$ et $initial$. Elles correspondent respectivement aux classes \texttt{Atom}, \texttt{True}, \texttt{False}, \texttt{Dead} et \texttt{Initial}. Comme leur implémentation est assez simple puisqu'elle n'ont pas de sous-preuves, on montrera juste les affichages obtenus au format textuel (figure \ref{fig:PreuveAtomiqueTextuel}) et au format \texttt{.dot} (figure \ref{fig:PreuveAtomiqueDot}) (sauf pour $false$ qui ne peut pas être affichée).

\input{"Rapport/preuve_atomique_textuel.tex"}

\input{"Rapport/preuve_atomique_dot.tex"}

\subsection{Preuves successeurs}

\subsubsection{$EX$}

Lors du coupage, une preuve de type $EX$ ne va garder qu'un seul état valide de la sous-preuve puisqu'il suffit de prouver que la formule est vraie pour un état voisin (figure \ref{fig:PreuveVoisinsEX}).

\input{"Rapport/preuve_voisins_ex.tex"}

\subsubsection{$AX$}

Lors du coupage, une preuve de type $AX$ va dupliquer plusieurs fois la sous-preuve pour chaque état la validant et étant un successeur (figure \ref{fig:PreuveVoisinsAX}). On simplifie ainsi les choses car une sous-preuve qui avait plusieurs états valides se retrouve en plusieurs exemplaires avec un seul état à chaque fois. Les autres preuves plus complexes seront donc justifiées uniquement sur un état.

\input{"Rapport/preuve_voisins_ax.tex"}

\subsection{Preuves chemins}

Les preuves qui consistent en un chemin d'états implémentent l'interface \texttt{IChemin} (listing \ref{lst:IChemin}) qui est elle-même basée sur \texttt{IPreuve}.

La structure d'un chemin consiste en la preuve pour l'état de départ (\texttt{getDebut}), celle pour l'état d'arrivée (\texttt{getFin}) et la liste des états par lesquels on passe (\texttt{getChemins}). Il n'y a qu'un seul état d'arrivée car, par exemple, si on doit prouver $AF(\cdots)$ pour plusieurs états, on va décomposer la preuve en plusieurs sous-preuves $AF(\cdots)$ pour chaque état (figure \ref{fig:PreuveCheminAF}).

\input{"Rapport/preuve_chemin_af_decompose.tex"}

Un chemin dispose aussi des accesseurs \texttt{estFin} et \texttt{aVoisinFin} qui lui permettent de savoir si il doit continuer la preuve pour les états voisins ou non.

\subsubsection{$EU$}

Après avoir été créée, la preuve de type $EU$ contient la preuve pour les états validant la condition du chemin, celle pour les états validant la condition d'arrêt et la liste des états qui ont un tel chemin.

Le coupage de la preuve entraîne la création d'une liste de sous-preuves pour tous les états par lesquels le chemin passe. Pour ce faire, on sait que la preuve parent a été coupée et qu'on doit prouver le chemin à partir des états restants. On va donc utiliser la liste des états ayant un tel chemin et ne garder que ceux qui ont pour prédécesseurs un ou plusieurs états de départ. On continue d'appliquer cette technique jusqu'à avoir atteint un des états validant la condition d'arrêt du chemin. Une fois que c'est fait, on peut supprimer tous les états du chemin qui ne sont pas nécessaires.

L'affichage d'une preuve de type $EU$ consiste donc en la preuve de la condition de départ pour chaque état du chemin et de la condition d'arrêt pour l'état final (figure \ref{fig:PreuveCheminEU}). Pour l'affichage au format textuel, la liste des états est affichée entre deux accolades et chaque étape du chemin possède la même indentation (figure \ref{fig:PreuveCheminEUTextuel}).

\input{"Rapport/preuve_chemin_eu.tex"}

\subsubsection{$AU$}

Tout comme pour la preuve de type $EU$, la preuve de type $AU$ va créer une liste de sous-preuves pour chaque états du chemin. Cependant, cette liste consistera en la dupplication de la preuve pour chacun de ces états. Ainsi, pour chaque état on prouvera que pour tous les états voisins il existe aussi le chemin (figure \ref{fig:PreuveCheminAU}).

\input{"Rapport/preuve_chemin_au.tex"}

\subsubsection{$EF$}

Une preuve de type $EF$ est une preuve similaire à celle de type $EU$ à la différence qu'elle n'a pas de condition à vérifier sur l'ensemble du chemin. Ainsi, on utilise une preuve $EU$ pour laquelle tous les états du chemin doivent vérifier $true$ (figure \ref{fig:PreuveCheminEF}).

\input{"Rapport/preuve_chemin_ef.tex"}

\subsubsection{$AF$}

Comme pour la preuve de type $EF$, la preuve de type $AF$ utilise une preuve $AU$ pour laquelle tous les états du chemin doivent vérifier $true$ (figure \ref{fig:PreuveCheminAF}).

\input{"Rapport/preuve_chemin_af.tex"}

\subsubsection{$EG$}

La preuve de type $EG$ utilise une preuve $EU$ pour laquelle tous les états du chemin doivent vérifier la condition (figure \ref{fig:PreuveCheminEG}).

\input{"Rapport/preuve_chemin_eg.tex"}

\subsubsection{$AG$}

La preuve de type $AG$ utilise une preuve $AU$ pour laquelle tous les états du chemin doivent vérifier la condition (figure \ref{fig:PreuveCheminAG}).

\input{"Rapport/preuve_chemin_ag.tex"}

\subsection{Preuves opérateurs}

\subsubsection{$\&\&$}

La preuve de type $\&\&$ affiche les preuves des deux conditions pour les états qui la valident (figure \ref{fig:PreuveOperateurAnd}).

\input{"Rapport/preuve_operateur_and.tex"}

\subsubsection{$\|$}

La preuve de type $\|$ affiche la preuve d'une des deux conditions dans le cas où elles seraient toutes les deux valides ou bien la preuve de celle qui est vraie (figure \ref{fig:PreuveOperateurOr}).

\input{"Rapport/preuve_operateur_or.tex"}

\subsubsection{$\rightarrow$}

L'implication est affichée comme le $\&\&$ (figure \ref{fig:PreuveOperateurImply}).

\input{"Rapport/preuve_operateur_imply.tex"}

Cependant, avec l'implication, il peut n'y avoir aucun état validant la condition de gauche et dans ce cas on devra quand même prouver que l'implication est correcte. Pour ce faire, si la condition de gauche n'a aucun état valide alors on calcule la preuve de sa négation, et si la condition de droite est également fausse alors on calcule aussi la preuve de sa négation. Ainsi, l'affichage sera la preuve que la ou les conditions ne sont pas valides (figure \ref{fig:PreuveOperateurImply2}).

\input{"Rapport/preuve_operateur_imply2.tex"}

\subsubsection{$\leftrightarrow$}

L'équivalence est affichée comme le $\&\&$ (figure \ref{fig:PreuveOperateurEquivalent}). Et comme pour l'implication, si aucun état n'est valide pour les deux conditions alors on calcule les preuves de leur négation et on les affiche à la place.

\input{"Rapport/preuve_operateur_equivalent.tex"}

\subsection{Contre exemple}

Lorsque l'état indiqué par l'utilisateur n'est pas un état valide de la formule saisie, on affichage à la place la justification d'un contre exemple en partant du même état. Pour trouver ce contre exemple, on fait simplement la négation de la formule en parcourant de manière récursive l'arbre retourné par le parseur. On dispose alors d'une nouvelle formule au format textuel que l'on va pouvoir utiliser, comme si l'utilisateur l'avait entrée, pour afficher la justification.

Dans l'exemple ci-dessous (figure \ref{fig:PreuveContreExempleTextuel}), la formule $EX(\$D)$ n'était pas valide pour l'état 0 et a donc été transformée en la formule $AX(!\$D)$ qui est la négation de la première. Dans la console, l'utilisateur est prévenu par un message lui disant que la formule donnée n'était pas valide. Dans le graphe (figure \ref{fig:PreuveContreExempleDot}), le message \texttt{Contre exemple} est affiché sous le label de l'état de départ.

\input{"Rapport/preuve_contre_exemple.tex"}

\subsection{Preuve négation}

La preuve de la négation est similaire aux contre exemples. Si la négation est appliquée à une formule atomique et que la visualisation est donc directe, on se contente d'afficher la preuve telle quelle (figure \ref{fig:PreuveNegation}). Par contre, si la négation est appliquée à une formule complexe, on commence par récupérer la négation de la formule, puis on la justifie comme si elle avait été saisie par l'utilisateur (figure \ref{fig:PreuveNegation2}). Lors de la coupure, on dira que l'état de départ de cette nouvelle formule est l'état validant la négation et ainsi on obtiendra la justification de la négation pour l'état voulu.

\input{"Rapport/preuve_negation.tex"}

\input{"Rapport/preuve_negation2.tex"}

\section{Utilisation du programme}

\subsection{Invité de commande}

Par défaut, le programme s'utilise en invité de commande. Dans ce mode, il affiche le symbole \texttt{>} et attend la saisie d'une commande. Les commandes données sont parsées à l'aide d'un parseur généré par ANTLR (voir \texttt{principal/CommandLine.g}) qui va se charger d'appeler les méthodes correspondantes dans la classe \texttt{Main}.

Les commandes disponibles sont toutes celles demandées dans le sujet ainsi que quelques unes qui ont été ajoutées.

\subsection{Commandes}

\noindent\begin{tabularx}{\linewidth}{@{}l l X@{}}
load & <fichier.net> & charge le réseau de pétri depuis le fichier \\
graphe & & calcule le graphe des états accessibles \\
look & <etat> & affiche le marquage de l'état \\
succ & <etat> & affiche la liste des successeurs de l'état \\
todot & <fichier.dot> & exporte le graphe au format \texttt{.dot} dans le fichier \\
ctl & <formule> & affiche le nombre d'états validant la formule \\
ctl & <formule> <etat> & affiche $vrai$ si l'état valide la formule ou $faux$ \\
ctltodot & <formule> <fichier.dot> & exporte le graphe au format \texttt{.dot} en colorant les états qui valident la formule \\
Justifie & <formule> <etat> & affiche la preuve au format textuel que l'état valide la formule \\
Justifietodot & <formule> <etat> <fichier.dot> & exporte le graphe et la preuve que l'état valide la formule au format \texttt{.dot} dans le fichier \\
shell & & passe en mode shell \\
stop & & arrête le programme \\
\end{tabularx}

\subsection{Création d'un script}

Outre le mode invité de commande, il est possible de créer un script pour lancer le programme et lui faire exécuter un ensemble de commandes. Les différents exemples fournis avec le projet fonctionnent ainsi:\\

On lance le programme normalement avec \texttt{java -jar modelprojet.jar} et on lui donne une liste de paramètres entre les deux balises \texttt{END\_PARAMS}.
\begin{verbatim}
java -jar modelprojet.jar << -END_PARAMS
    ...
END_PARAMS
\end{verbatim}

On commence par exécuter la commande \texttt{shell} qui permet au programme de passer en mode shell. Dans ce mode, toutes les commandes exécutées sont affichées après le symbole \texttt{>}. Ce mode est nécessaire car les commandes fournies au programme entre les balises \texttt{END\_PARAMS} ne sont pas affichées dans la console comme si elles avaient été saisies par l'utilisateur. La dernière commande à exécuter doit être la commande \texttt{stop} pour demander au programme de s'arrêter une fois le script fini.

\begin{verbatim}
java -jar modelprojet.jar << -END_PARAMS
    shell
    ...
    stop
END_PARAMS
\end{verbatim}

C'est entre les deux commandes \texttt{shell} et \texttt{stop} que l'on peut ajouter toutes les commandes du script.

\begin{verbatim}
java -jar modelprojet.jar << -END_PARAMS
    shell
    load "hello.net"
    graphe; todot "hello.dot"
    ctl EX(EX(\$C)); ctl EX(\$C)
    stop
END_PARAMS
\end{verbatim}

\`{A} noter que des commandes séparées par un retour à la ligne produiront le même effet que si l'utilisateur avait saisi la première, appuyé sur entrée puis avait saisi la seconde. \`{A} l'inverse, deux commandes séparées par une point-virgule seront parsées et exécutées à la suite comme si elles avaient été saisies en même temps par l'utilisateur.

La différence est que, dans le second cas, les résultats des deux commandes seront affichés à la suite sans savoir quelle commande a produit quel résultat. Alors que dans le premier cas, le résultat de la première commande sera séparé du résultat de la seconde par le symbole \texttt{>} et l'affichage de la seconde commande.

\section{Exemples}

De nombreux exemples ont été créés et sont disponibles dans le dossier d'exemples du projet. Ces exemples sont sous la forme d'un script \texttt{.sh} qui doit se trouver dans le même dossier que le \texttt{.jar} du programme.\\

Chaque exemple contient des commentaires indiquant son intérêt et les fichiers produits. Cependant, voici une liste récapitulative des plus importants:\\

\noindent\begin{tabularx}{\linewidth}{| @{}l | X@{} |}
\hline
Script \texttt{.sh} & Description \\
\hline
test commandes & exécute toutes les commandes demandées dans le sujet sur le fichier \texttt{hello.net} \\
\hline
test justifie & produit une justification au format textuel et \texttt{.dot} de l'ensemble des formules possibles sur les différents fichiers \texttt{.net} \\
\hline
preuves atomiques & produit une justification au format textuel et \texttt{.dot} des formules atomiques $p$, $true$, $dead$ et $initial$ sur le fichier \texttt{atomique.net} \\
\hline
preuves voisins & produit une justification au format textuel et \texttt{.dot} des formules atomiques $EX$ et $AX$ sur le fichier \texttt{chemin.net} \\
\hline
preuves chemins & produit une justification au format textuel et \texttt{.dot} des formules atomiques $EU, AU, EF, AF, EG$ et $AG$ sur les fichiers \texttt{chemin.net} et \texttt{chemin2.net} \\
\hline
preuves operateurs & produit une justification au format textuel et \texttt{.dot} des formules atomiques $\&\&, \|, \rightarrow$ et $\leftrightarrow$ sur le fichier \texttt{operateur.net} \\
\hline
contre exemple & évalue chaque formule  $p, true, initial, \cdots, EX, \cdots, EF, \cdots$ sur un état du rdp \texttt{chemin.net} pour lequel elle n'est pas valide afin d'afficher le contre exemple. \\
\hline
\end{tabularx}

~\\\indent Quelques exemples concrets:\\

\noindent\begin{tabularx}{\linewidth}{| @{}l | X@{} |}
\hline
Script \texttt{.sh} & Description \\
\hline
indiana & affiche, dans \texttt{indiana ctl.dot}, les états qui ont un chemin vers la solution et, dans \texttt{indiana justifie.dot}, la preuve qu'il est possible d'atteindre la solution depuis l'état 0 \\
\hline
Chameaux3 & même chose mais avec l'exemple des chameaux \\
\hline
aspirateur & affiche, dans \texttt{aspirateur ctl.dot}, les états qui ont un chemin vers un état où l'aspirateur a nettoyé les deux cases et, dans \texttt{aspirateur justifie.dot}, la preuve qu'il est possible d'atteindre un tel état depuis l'état 6 \\
\hline
\end{tabularx}

\newpage

\begin{lstlisting}[caption={Interface \psverb+ICallback+}, label={lst:ICallback}]
public interface ICallback {

	public RdP getRdP();	
	public void shell();
	public void load(String filename);
	public void graphe();
	public void look(int etat);
	public void succ(int etat);
	public void toDot(String filename);
	public void ctl(Tree formule);
	public void ctl(Tree formule, int etat);
	public void ctlToDot(Tree formule, String filename);
	public void justifie(Tree formule, int etat);
	public void justifieToDot(Tree formule, int etat, String filename);
	public void stop();

}
\end{lstlisting}

\begin{lstlisting}[caption={Interface \psverb+IPreuve+ commune à toutes les preuves}, label={lst:IPreuve}]
public interface IPreuve {

	public Tree getFormule();
	public boolean[] getMarquage();
	public void setMarquage(boolean[] marquage);
	public List<IPreuve> getPreuves();

	public void couperRacine(CTL ctl, int[][] pred, int etat);
	public void couper(CTL ctl, int[][] pred, boolean[] parents);

	public String toTree();
	public String toTree(String indent);

	public void toDotRacine(Map<Integer, Set<Integer>> fleches,
			Set<String> justifications, IPreuve parent, int etatParent,
			Coloration couleurs);
	public void toDot(Map<Integer, Set<Integer>> fleches,
			Set<String> justifications, IPreuve parent, int etatParent,
			Coloration couleurs);

	public String toDotLabel(Coloration couleurs);
	public IPreuve clone();
	public String formuleToString();

}
\end{lstlisting}

\begin{lstlisting}[caption={Classe \psverb+Coloration+}, label={lst:Coloration}]
public class Coloration {

	private Map<Tree, String> couleursFormules;
	private Map<Tree, String> labelsFormules;

	public String getCouleur(Tree formule);
	public String getLabel(Tree formule);

	public void ajouter(Tree formule, String couleur, String label);
	public FakeTree ajouter(String label);

	public String genererCouleur();

}
\end{lstlisting}

\newpage
\begin{lstlisting}[caption={Interface \psverb+IChemin+}, label={lst:IChemin}]
public interface IChemin extends IPreuve {

	List<boolean[]> getChemins();

	IPreuve getDebut();
	void setDebut(IPreuve preuve);

	IPreuve getFin();
	void setFin(IPreuve preuve);

	boolean estFin();
	boolean aVoisinFin();

}
\end{lstlisting}

\end{document}